Inference at * 
Iof proof for Lemma member-assert:


  b:. (b)  (Ax  (b)) 

latex

 by ((D (0)) 
CollapseTHENA (Auto)) 
CollapseTHEN ((AutoBoolCase b ) 
CollapseTHEN ((Try ((
CUnfolds ``it true`` ( 0)) 
CollapseTHEN ((Complete (Auto))))))) 

latex

C.

Definitions	left + right, P  Q, P & Q, x:A  B(x), , s = t, b, A, , x:AB(x), b, Unit, False, True, , P  Q, Ax, x:A. B(x), , t  T, #$n
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, true wf, it wf, false wf, member wf